A, B:MsgA. ma-is-empty(A)  A  B 

latex

Definitions	t  T, x:A. B(x), M1  M2, , MsgA, Prop, P  Q, ma-is-empty(M), b, P  Q, P & Q, P  Q, {T}, x. t(x)
Lemmas	all functionality wrt iff, implies functionality wrt iff, assert-ma-is-empty, assert wf, ma-is-empty wf, ma-empty wf, msga wf, ma-sub wf, ma-empty-sub